With the advent of agile software engineering methodologies and rapid development lifecycles, software quality assurance has proven to be a daunting task. Quality assurance tools such as bug-checkers and software model checkers play an important role in maintaining software quality.
Model checking (MC) is a formal methods technique used for the verification of hardware and software systems. Model checking algorithmically verifies behaviors of a system against one or more pre-defined properties or defect types. These systems are commonly represented as finite-state machines (FSM). Systems may be abstracted as finite-state machines so they can be tested in a mathematical and concrete fashion whereas properties of the system are sometimes expressed in Linear Temporal Logic (LTL) or Computation Tree Logic (CTL) formulas. A Software Model Checker (SMC) may be used to perform algorithmic verification of the FSM.
In a software example, a bug-checking tool builds a model to represent a given software program. This model may be an abstraction depicting the behavior of the software program. An SMC may then check the model against a specification including pre-defined error conditions and program properties. Based on the specification, the SMC is able to verify whether the system satisfies a specified property (e.g., an error state). Due to the combinatorial nature of model checking algorithms, the memory and processing power required to complete an analysis of the model can increase exponentially with the number of states.